<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html lang="EN-US">
<head>
  <meta http-equiv="Content-Type"
 content="text/html; charset=ISO-8859-1">
  <style type="text/css">
  </style>
</head>

<body bgcolor="#ffffff">

<span style="font-family: monospace;">
$(&nbsp;&lt;MM&gt;&nbsp;&lt;PROOF&nbsp;ASST&gt;&nbsp;THEOREM=</span>

<span style="font-family: monospace;">
<a href="..\html\syl.html">syl</a></span>

<span style="font-family: monospace;">
&nbsp;LOC_AFTER=</span><br>

<span style="font-family: monospace;">
&nbsp;</span><br>

<span style="font-family: monospace;">
* An inference version of the transitive laws for implication ~ imim2 and</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;~ imim1 , which Russell and Whitehead call "the principle of the</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;syllogism...because...the syllogism in Barbara is derived from them"</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;(quote after Theorem *2.06 of [WhiteheadRussell] p. 101).  Some authors</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;call this law a "hypothetical syllogism."</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;(A bit of trivia: this is the most commonly referenced assertion in our</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;database.  In second place is ~ ax-mp , followed by ~ visset , ~ bitri ,</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;~ imp , and ~ ex .  The Metamath program command 'show usage' shows the</span><br>

<span style="font-family: monospace;">
&nbsp;&nbsp;number of references.)</span><br>

<span style="font-family: monospace;">
&nbsp;</span><br>


<span style="font-family: monospace;">
h1::syl.1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
<FONT COLOR="#808080" FACE=sans-serif>&#8866; </FONT>
(
<FONT COLOR="#0000FF"><I>&phi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&psi;</I></FONT>
)
<br>


<span style="font-family: monospace;">
h2::syl.2&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
<FONT COLOR="#808080" FACE=sans-serif>&#8866; </FONT>
(
<FONT COLOR="#0000FF"><I>&psi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&chi;</I></FONT>
)
<br>


<span style="font-family: monospace;">
3:2:a1i&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
<FONT COLOR="#808080" FACE=sans-serif>&#8866; </FONT>
(
&nbsp;
<FONT COLOR="#0000FF"><I>&phi;</I></FONT>
<br>

<span style="font-family: monospace;">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
 &rarr;
(
<FONT COLOR="#0000FF"><I>&psi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&chi;</I></FONT>
)
)
<br>

<span style="font-family: monospace;">
4:3:a2i&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
<FONT COLOR="#808080" FACE=sans-serif>&#8866; </FONT>
(
&nbsp;
(
<FONT COLOR="#0000FF"><I>&phi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&psi;</I></FONT>
)
<br>

<span style="font-family: monospace;">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
 &rarr;
(
<FONT COLOR="#0000FF"><I>&phi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&chi;</I></FONT>
)
)
<br>

<span style="font-family: monospace;">
qed:1,4:ax-mp&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span>
<FONT COLOR="#808080" FACE=sans-serif>&#8866; </FONT>
(
<FONT COLOR="#0000FF"><I>&phi;</I></FONT>
 &rarr;
<FONT COLOR="#0000FF"><I>&chi;</I></FONT>
)
<br>

<span style="font-family: monospace;">
&nbsp;</span><br>

<span style="font-family: monospace;">
$)
</span><br>

</body>
</html>
